
import Debug.QuickCheck
import System.Directory
import List

-------------------------------------------------------------------------
-- 1. Properties of the look function

type Table a b = [(a,b)]

look :: Eq a => a -> Table a b -> Maybe b
look x []           = Nothing
look x ((x',y):xys)
  | x == x'         = Just y
  | otherwise       = look x xys

prop_LookJust :: Integer -> [(Integer,Integer)] -> Property
prop_LookJust x xys =
  look_x /= Nothing ==>
    (x,y) `elem` xys
 where
  look_x = look x xys
  Just y = look_x

prop_Look :: Integer -> [(Integer,Integer)] -> Bool
prop_Look x xys =
  examine (look x xys)
 where
  examine Nothing  = x `notElem` [ x | (x,_) <- xys ]
  examine (Just y) = (x,y) `elem` xys

-------------------------------------------------------------------------
-- 2. Pascal's Triangle

pascal :: Int -> [Int]
pascal 1 = [1]
pascal n = [1] ++ [ x+y | (x,y) <- pairs (pascal (n-1)) ] ++ [1]
 where
  pairs (x:y:xs) = (x,y) : pairs (y:xs)
  pairs _        = []

prop_Pascal n =
  n >= 1 ==>
    length (pascal n) == n

-------------------------------------------------------------------------
-- 3. Eratosthenes' sieve

crossOut :: Int -> [Int] -> [Int]
crossOut n xs = [ x | x <- xs, x `mod` n /= 0 ]

sieve :: [Int] -> [Int]
sieve []     = []
sieve (n:ns) = n : sieve (crossOut n ns)

primes1to100 = sieve [2..100]

prop_Sieve n =
  and [ isPrime n | n <- sieve [2..n] ]
 where
 isPrime n = factors n == [1,n]
 factors n = [ k | k <- [1..n], n `mod` k == 0 ]

-------------------------------------------------------------------------
-- 4. Number Games

isPrime100 :: Int -> Bool
isPrime100 n = n `elem` primes1to100

isSumOf2Primes100 :: Int -> Bool
isSumOf2Primes100 n =
  not (null [ (a,b)
            | a <- primes1to100
            , b <- primes1to100
            , n == a+b
            ])

counterExamples :: [Int]
counterExamples = [ n | n <- [4..100], even n, not (isSumOf2Primes100 n) ]

prop_Goldbach =
  null counterExamples

-------------------------------------------------------------------------
-- 5. Occurrences in Lists

occursIn :: Eq a => a -> [a] -> Bool
occursIn x xs = x `elem` xs

allOccurIn :: Eq a => [a] -> [a] -> Bool
allOccurIn xs ys = and [ x `elem` ys | x <- xs ]

sameElements :: Eq a => [a] -> [a] -> Bool
sameElements xs ys = allOccurIn xs ys && allOccurIn ys xs

numOccurIn :: Eq a => a -> [a] -> Int
numOccurIn x xs = length [ x' | x' <- xs, x == x' ]

type Bag a = Table a Int

bag :: Eq a => [a] -> Bag a
bag xs = [ (x, numOccurIn x xs) | x <- nub xs ]

isPermutation :: Eq a => [a] -> [a] -> Bool
isPermutation []     []     = True
isPermutation []     (y:ys) = False
isPermutation (x:xs) ys     = x `elem` ys && isPermutation xs (remove1 x ys)

prop_Bag :: [Int] -> Bool
prop_Bag xs =
  [ x | (x,n) <- bag xs, i <- [1..n] ] `isPermutation` xs

{-
Note that

  [ x | (x,n) <- xns, i <- [1..n] ]
  
is a list of all elements in the bag xns, where all elements are repeated
the number of times they occur in the bag xns.
-}

-------------------------------------------------------------------------
-- 6. Elements and Positions

positions :: [a] -> [(a,Int)]
positions xs = xs `zip` [1..length xs]

{-
-- alternatively:
positions :: [a] -> [(a,Int)]
positions xs = xs `zip` [1..]
-}

firstPosition :: Eq a => a -> [a] -> Int
firstPosition x xs = head [ i | (x',i) <- positions xs, x' == x ]

prop_FirstPositionIsX :: Int -> [Int] -> Property
prop_FirstPositionIsX x xs =
  x `elem` xs ==>
    xs !! (firstPosition x xs - 1) == x
    
prop_FirstPositionIsFirst :: Int -> [Int] -> Property
prop_FirstPositionIsFirst x xs =
  x `elem` xs ==>
    and [ x /= x' | x' <- take (firstPosition x xs - 1) xs ]
    
{-
Here, the function (!!) is a standard function: xs !! i produces the ith element
from the list xs. Counting starts at 0.

Furthermore, take n xs produces the first n elements of the list xs.
-} 

remove1 :: Eq a => a -> [a] -> [a]
remove1 = removen 1

removen :: Eq a => Int -> a -> [a] -> [a]
removen 0 _ ys                 = ys
removen _ _ []                 = []
removen n x (y:ys) | x == y    = removen (n-1) x ys
                   | otherwise = y : removen n x ys

prop_RemoveN n x xs =
  length (xs \\ removen n x xs) <= n

prop_RemoveNOnlyX n x xs =
  and [ x == x' | x' <- xs \\ removen n x xs ]

{-
Here, the function (\\) is a standard function: xs \\ ys removes each element
in ys once from xs.
-} 

-------------------------------------------------------------------------
-- 7. More List Comprehensions

pythagoreanTriads :: [(Int,Int,Int)]
pythagoreanTriads = [ (a,b,c)
                    | a <- [1..100]
                    , b <- [1..100]
                    , c <- [1..100]
                    , a^2 + b^2 == c^2
                    ]

{-
A more efficient version, that also leaves out symmetric solutions
(such as (3,4,5) and (4,3,5)) is:
-}

pythagoreanTriads' :: [(Int,Int,Int)]
pythagoreanTriads' = [ (a,b,c)
                     | a <- [1..100]
                     , b <- [a..100]
                     , let c2 = a^2 + b^2
                           c  = floor (sqrt (fromIntegral c2))
                     , c <= 100
                     , c^2 == c2
                     ]

{-
Note: Browse the Haskell libraries, and use Hugs to see what type the
functions floor, sqrt and fromIntegral have and what they do.
-}

prop_Pythagoras =
  and [ (a,b,c) `elem` pythagoreanTriads
      | (a,b,c) <- pythagoreanTriads'
      ]

prop_Pythagoras' =
  and [ (a,b,c) `elem` pythagoreanTriads'
     || (b,a,c) `elem` pythagoreanTriads'
      | (a,b,c) <- pythagoreanTriads
      ]

-------------------------------------------------------------------------
-- 8. Majority Governments

{-
From the lecture:
-}

data Parti
  = V
  | S
  | Mp
  | C
  | Fp
  | Kd
  | M
 deriving ( Eq, Ord, Show )

type Mandat = Integer

riksdag :: [(Parti,Mandat)]
riksdag =
  [ (V,   22)
  , (S,  130)
  , (Mp,  19)
  , (C,   29)
  , (Fp,  28)
  , (Kd,  24)
  , (M,   97)
  ]

type Regering = [Parti]

-- the definition from the lecture
majorities' :: [(Parti,Mandat)] -> [Regering]
majorities' riks = need 175 riks
 where
  need man _ | man <= 0        = [[]]
  need man []                  = []
  need man ((parti,man'):riks) =
    need man riks ++
      [ parti : block | block <- need (man-man') riks ]

prop_MajoritiesHaveMajority riks =
  and [ sum [ man | (parti,man) <- riks, parti `elem` reg ] >= 175
      | reg <- majorities riks
      ]

{-
The solution is to let the need function also compute the number of parlament
seats for each government solution.

We then only add a party when we actually need to.

Note that the type of need has changed, and we throw away that extra information
at the top-level.

We still have three cases in need:

* When no seats are required, the empty government with no seats is enough (one
element list of with one zero-party government and no seats)

* When no parties are left, we cannot form a government (empty list of
governments)

* Otherwise, when we have at least one party parti with man' seats, we can
either form a government with man seats without that party at all
(using "need man riks"), or we form a government with man-man' seats using the
rest of the parlament. We then add the party parti, but only if the total number
of seats of that government is not enough.
-}

majorities :: [(Parti,Mandat)] -> [Regering]
majorities riks = [ block | (block,_) <- need 175 riks ]
 where
  need :: Mandat -> [(Parti,Mandat)] -> [([Parti],Mandat)]
  need man _ | man <= 0        = [([],0)]
  need man []                  = []
  need man ((parti,man'):riks) =
    need man riks ++
      [ (parti : block, total+man')
      | (block,total) <- need (man-man') riks
      , total < man
      ]

prop_MajoritiesAreMinimal riks =
  and [ sum [ man
            | (parti,man) <- riks
            , parti `elem` reg
            , parti /= parti'
            ] < 175
      | reg <- majorities riks
      , parti' <- reg
      ]

-------------------------------------------------------------------------
-- 9. 

listOf :: Int -> Gen a -> Gen [a]
listOf n gen = sequence [ gen | i <- [1..n] ]

pairsOfEqualLengthLists :: Gen a -> Gen ([a],[a])
pairsOfEqualLengthLists gen =
  do n <- arbitrary
     xs <- listOf (abs n) gen
     ys <- listOf (abs n) gen
     return (xs,ys)

prop_ZipUnzip :: [(Int,Int)] -> Bool
prop_ZipUnzip xys =
  zip xs ys == xys
 where
  (xs,ys) = unzip xys
     
prop_UnzipZip :: [Int] -> [Int] -> Property
prop_UnzipZip xs ys =
  length xs == length ys ==>
    unzip (zip xs ys) == (xs,ys)
     
prop_UnzipZip' :: Property
prop_UnzipZip' =
  forAll (pairsOfEqualLengthLists arbitrary) $ \(xs,ys) ->
    unzip (zip xs ys) == (xs :: [Int],ys :: [Int])
     
-------------------------------------------------------------------------
-- 10. 

backup :: IO ()
backup =
  do files <- getDirectoryContents "."
     createDirectory "backup"
     sequence_
       [ copyFile' file ("backup/" ++ file)
       | file <- files
       ]     

-- copyFile' file file' copies file to file', if file is a real file
-- (and not a directory)
copyFile' :: FilePath -> FilePath -> IO ()
copyFile' file file' =
  do isFile <- doesFileExist file
     if isFile
       then copyFile file file'
       else return ()
